p =b q == (p  q) ((p)  (q)) 

latex

Up	bool 1, bool 1
Wellformedness Lemmas	eq bool wf, eq bool wf
Definitions	p q, p  q, b
FDL editor aliases	eq_bool